es:ES, Cmd:Type, Sys:AbsInterface(chain_sys(Cmd)).
input-dcdr{i:l}(es;Cmd;Sys)  e:EDec(((e  Sys)) c (csinput?(Sys(e)))) 

latex

Definitions

t  T, s = t, x:AB(x), x:A. B(x), chain_sys(Cmd), e  X, b, Type, , ES, AbsInterface(A), E, decidable input, f(a), X(e), csinput?(x), x:A  B(x), A c B, Dec(P), {x:A| B(x)} , E(X), a:A fp B(a), strong-subtype(A;B), P  Q, left + right, let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , , Id, type List, Unit, ff, inr x , "$token", tt, inl x , Atom, Top, False, True, A, EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd, x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), P & Q, loc(e), kind(e), SWellFounded(R(x;y)), pred!(e;e'), Void, x:A.B(x), S  T, suptype(S; T), first(e), <a, b>, pred(e), x.A(x), input-dcdr{i:l}(es;Cmd;Sys)

Lemmas

decidable input, kind wf, loc wf, first wf, pred! wf, strongwellfounded wf, constant function wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, deq wf, event system wf, not wf, decidable wf, true wf, false wf, top wf, btrue wf, bfalse wf, unit wf, bool wf, csinput? wf, es-interface-val wf, Id wf, es-interface wf, es-interface-val wf2, member wf, es-E-interface wf, es-E wf, subtype rel wf, assert wf, chain sys wf, es-is-interface wf